ds:x:Id fp Type, da:k:Knd fp Type, v:ecl-trans-tuple{i:l}(ds;da).
ecl-trans-normal(v)
 (L':event-info(ds;da) List.
 ((L:event-info(ds;da) List. L  L'  ecl-trans-halt2(ds;da;v)(0,L)  False)
 ( ecl-trans-state(reset-ecl-tuple(v);L')
 ( =
 ( ecl-trans-state(v;L')
 (  ecl-trans-type(reset-ecl-tuple(v))) 

latex

Definitions

Id, t  T, x. t(x), x:A. B(x), a:A fp B(a), Knd, ecl-trans-tuple{i:l}(ds;da), ecl-trans-normal(x), event-info(ds;da), AB, P  Q, False, A, , Prop, ecl-trans-halt2(ds;da;A), l1  l2, ecl-trans-state(v;L), reset-ecl-tuple(A), ecl-trans-type(A), Valtype(da;k), KindDeq, (x  l), b, b, , deq-member(eq;x;L), P & Q, P  Q, Unit, State(ds), Top, f(x)?z, if b t else f fi, x,y. t(x;y), list_accum(x,a.f(x;a);y;l), as @ bs, let a,b,c,d,e,f,g = u in v(a;b;c;d;e;f;g), ecl-trans-state-from(v;z;L), ecl-trans-init(v), S  T, ecl-trans-h(v)

Lemmas

list accum append, decl-state wf, fpf-cap wf, top wf, list accum functionality, append wf, list accum wf, ifthenelse wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert-deq-member, deq-member wf, bool wf, bnot wf, not wf, assert wf, l member wf, Kind-deq wf, iseg wf, ecl-trans-halt2 wf, false wf, le wf, event-info wf, ecl-trans-normal wf, ecl-trans-tuple wf, Knd wf, fpf wf, Id wf